Inference at * 1 3 
Iof proof for Lemma decidable equal bool:



  (tt = ff)  ((tt = ff)) 

latex

 by ((((Sel 2 (D 0)) 
CollapseTHENM (BLemma `btrue_neq_bfalse`))) 
CollapseTHEN (
C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C.

Definitions	, t  T, P  Q
Lemmas	bfalse wf, btrue wf, bool wf, btrue neq bfalse